<html>
<head><meta charset="utf-8"><title>Understanding the Polonius model · t-compiler/wg-polonius · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/index.html">t-compiler/wg-polonius</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html">Understanding the Polonius model</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="232761511"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232761511" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232761511">(Apr 01 2021 at 14:04)</a>:</h4>
<p>Hi Polonius team, after a productive thread (<a class="stream-topic" data-stream-id="122651" href="/#narrow/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing">#general &gt; Relationship between lifetimes and aliasing</a>) I've set out to better understand the Polonius model. A first question: would you agree with this statement?</p>
<blockquote>
<p>In the Polonius model of borrows, the borrow checker is an abstract interpreter that computes the set of possible locations that a pointer can have at any point in the program.</p>
</blockquote>
<p>I realize that doesn't include details about whether the loans are mutable and whether loan terms are violated. But it struck me that Polonius looks much more like an abstract interpreter than the classic borrow checker does.</p>



<a name="232762938"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232762938" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232762938">(Apr 01 2021 at 14:12)</a>:</h4>
<p>Also, importantly Polonius is (in a way) a _flow-insensitive_ data analysis because the set of possible loans is accumulated across all points, rather than computed differently for each point. Therefore a reference's region has a single value, rather than a different value per point. </p>
<p>But that description doesn't seem to take into account the refinement of <code>subset</code>/<code>requires</code> as described in Niko's blog post: <a href="http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/#refining-constraint-propagation-with-liveness">http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/#refining-constraint-propagation-with-liveness</a></p>



<a name="232816641"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232816641" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232816641">(Apr 01 2021 at 20:03)</a>:</h4>
<p><span class="user-mention silent" data-user-id="265377">Will Crichton</span> <a href="#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Understanding.20the.20Polonius.20model/near/232761511">said</a>:</p>
<blockquote>
<p>Hi Polonius team, after a productive thread (<a class="stream-topic" data-stream-id="122651" href="/#narrow/stream/122651-general/topic/Relationship.20between.20lifetimes.20and.20aliasing">#general &gt; Relationship between lifetimes and aliasing</a>) I've set out to better understand the Polonius model. A first question: would you agree with this statement?</p>
<blockquote>
<p>In the Polonius model of borrows, the borrow checker is an abstract interpreter that computes the set of possible locations that a pointer can have at any point in the program.</p>
</blockquote>
</blockquote>
<p>Yes. This is exactly what Prusti exploits for verification.</p>



<a name="232816745"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232816745" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232816745">(Apr 01 2021 at 20:04)</a>:</h4>
<p>Just it is important to note that when you cross the function boundary, the lifetimes act as a way to abstract over possible locations.</p>



<a name="232817110"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232817110" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232817110">(Apr 01 2021 at 20:06)</a>:</h4>
<p><span class="user-mention silent" data-user-id="265377">Will Crichton</span> <a href="#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Understanding.20the.20Polonius.20model/near/232762938">said</a>:</p>
<blockquote>
<p>Also, importantly Polonius is (in a way) a _flow-insensitive_ data analysis because the set of possible loans is accumulated across all points, rather than computed differently for each point. Therefore a reference's region has a single value, rather than a different value per point. </p>
</blockquote>
<p>This sounds wrong to me, probably I do not understand what you mean. Could you give an example?</p>



<a name="232817440"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232817440" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232817440">(Apr 01 2021 at 20:09)</a>:</h4>
<p>In Polonius, <code>loan_live_at(L, P)</code> is computed for each program point <code>P</code> as described in Niko's <a href="http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/">blog post</a>.</p>



<a name="232819494"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232819494" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232819494">(Apr 01 2021 at 20:24)</a>:</h4>
<p><span class="user-mention" data-user-id="116109">@Vytautas Astrauskas [he/him]</span> thanks for the clarification. And actually the flow-sensitive part isn't super important, so don't worry about that.</p>
<p>But I do actually have a question for you -- I'm trying to write an OOPSLA paper about my Rust program slicer. One goal is to create a more formal argument for why the borrow checker's information is sufficient to conservatively estimate the aliases for any borrow (at the MIR level). Do you know of any related work that makes a similar argument? I've checked out Prusti, RustBelt, and Oxide but none seems quite appropriate -- Prusti focuses on encoding into Viper, RustBelt focuses on implications of unsafe and uses an outdated notion of lifetimes, and Oxide focuses on surface-level Rust and not MIR.</p>



<a name="232820242"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232820242" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232820242">(Apr 01 2021 at 20:30)</a>:</h4>
<p>My current intuition (and the relevance to Polonius) is to make the following argument:</p>
<ul>
<li>MIR pointers have an unknown "true provenance", or the set of loans they can actually refer to in any possible execution of the program</li>
<li>
<p>Pointers are annotated with a provenance variable, and the borrow checker tells us two things about provenance variables: </p>
<ol>
<li>if the provenance variable is the direct result of a loan (ie an &amp;p rvalue)</li>
<li>outlives relations between the provenance variable and other provenance variables</li>
</ol>
</li>
<li>
<p>A pointer's approximate provenance can be computed as the union of the approximate provenance of all pointers that outlive it plus any direct loans</p>
</li>
<li>If the borrow checker correctly computes the necessary set of outlives relations, then a pointer's approximate provenance is a superset of the true provenance, and hence a sound approximation to the aliases of the pointer</li>
</ul>



<a name="232820968"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232820968" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232820968">(Apr 01 2021 at 20:35)</a>:</h4>
<p>I'm trying to figure out:<br>
a) is this argument correct?<br>
b) if so, do I need to define my own  MIR formalism, or I can reuse one like e.g. in RustBelt<br>
c) which parts of this argument have already been made in related work vs. I need to justify myself<br>
d) how to precisely talk about the "necessary set of outlives relations", ie the sufficient condition that rustc must meet for alias analysis to be correct</p>



<a name="232822490"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232822490" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232822490">(Apr 01 2021 at 20:46)</a>:</h4>
<blockquote>
<p>One goal is to create a more formal argument for why the borrow checker's information is sufficient to conservatively estimate the aliases for any borrow (at the MIR level).</p>
</blockquote>
<p>Isn't this basically an argument that the Rust type system is sound?</p>



<a name="232822691"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232822691" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232822691">(Apr 01 2021 at 20:48)</a>:</h4>
<p>Or to phrase it differently: if the borrow checker's information would not be sufficient, I, think, that would imply that the Rust type system is unsound.</p>



<a name="232823135"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232823135" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232823135">(Apr 01 2021 at 20:51)</a>:</h4>
<blockquote>
<p>RustBelt focuses uses an outdated notion of lifetimes</p>
</blockquote>
<p>I would not agree with this. Even though the paper was written before NLL and Polonius, I think the presented approach is flexible enough to handle most examples. I know that there are problems with two-phase borrows, but that is the only limitation I remember.</p>



<a name="232825264"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232825264" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232825264">(Apr 01 2021 at 21:07)</a>:</h4>
<blockquote>
<p>a) is this argument correct?</p>
</blockquote>
<p>I do not see any mistakes, but it is also a bit late now for me to give a proper answer.</p>
<blockquote>
<p>b) if so, do I need to define my own MIR formalism, or I can reuse one like e.g. in RustBelt</p>
</blockquote>
<p>This literary looks like you are trying to prove the soundness of Polonius. One option would be to try to prove it against operational semantics, which would be <a href="https://www.ralfj.de/blog/2019/11/18/stacked-borrows-paper.html">Stacked Borrows</a>.</p>
<blockquote>
<p>c) which parts of this argument have already been made in related work vs. I need to justify myself</p>
</blockquote>
<p>Do you actually need to? Cannot you just assume the correctness of the compiler?</p>



<a name="232825294"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232825294" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232825294">(Apr 01 2021 at 21:07)</a>:</h4>
<p>Re: the type system, I agree, and part of the point is to elucidate the link between alias analysis and Rust's type system.  Rust doesn't actually compute aliases and use them in type checking, so it's not immediately obvious that the borrow checker outputs are sufficient to compute aliases.</p>
<p>And yes I don't meant to imply that the RustBelt formalism is no longer useful. But rather the connection between borrows and aliases is much clearer (I think) when lifetimes are provenances (ie set of loans) instead of regions (sets of locations).</p>



<a name="232825702"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232825702" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232825702">(Apr 01 2021 at 21:10)</a>:</h4>
<p>One key bit is that I'd like to articulate this point in a way that's distinct from whether Rust is using classic borrow checking, NLL, or Polonius. I want to say "if a compiler infers at least the right set of outlives constraints, then this method of computing aliases is sound" and then make a high-level argument as to why any particular version of the borrow checker infers the "right" set of constraints.</p>



<a name="232825894"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232825894" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232825894">(Apr 01 2021 at 21:12)</a>:</h4>
<p>Couldn't you make an argument that if the borrow checker would not do a proper over-approximation of aliases, the type system would be unsound?</p>



<a name="232825965"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232825965" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232825965">(Apr 01 2021 at 21:13)</a>:</h4>
<p>I do not think you can have the same proof for all three versions of the borrow checker.</p>



<a name="232826182"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232826182" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232826182">(Apr 01 2021 at 21:14)</a>:</h4>
<blockquote>
<p>And yes I don't meant to imply that the RustBelt formalism is no longer useful. But rather the connection between borrows and aliases is much clearer (I think) when lifetimes are provenances (ie set of loans) instead of regions (sets of locations).</p>
</blockquote>
<p>As far as I understand RustBelt, it actually does not care which interpretation of lifetimes you take. It works with both.</p>



<a name="232826495"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Understanding%20the%20Polonius%20model/near/232826495" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Will Crichton <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Understanding.20the.20Polonius.20model.html#232826495">(Apr 01 2021 at 21:16)</a>:</h4>
<blockquote>
<p>Couldn't you make an argument that if the borrow checker would not do a proper over-approximation of aliases, the type system would be unsound?</p>
</blockquote>
<p>Yes this seems reasonable. I'll have to think about the argument, thanks for the suggestion.</p>
<blockquote>
<p>As far as I understand RustBelt, it actually does not care which interpretation of lifetimes you take. It works with both.</p>
</blockquote>
<p>Ok, I will see if I can make the argument above using the RustBelt model.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>